g:IGroup, a, b, c:|g|. ((a * b) = (a * c)  |g|)  (b = c) 

latex

Up	groups 1
Definitions of Statement	IMonoid, IGroup
Definitions	, t  T, x f y, P  Q, x:A. B(x), P  Q, P & Q, P  Q, IMonoid, IGroup
Lemmas	igrp wf, grp op wf, grp car wf, grp inv wf, grp op l, mon ident, grp inverse, mon assoc